1. ${\it xm}$ : $\forall$$P$:$\mathbb{P}$. $P$ $\vee$ ($\neg$$P$)
\\[0ex]2. $T$ : Type
\\[0ex]3. $P$ : $T$$\rightarrow\mathbb{P}$
\\[0ex]4. $\exists$$a$:$T$. $P$($a$)
\\[0ex]5. $z$ : \{$y$:$T$$\mid$ $P$($y$)\}  $\vee$ ($\neg$\{$y$:$T$$\mid$ $P$($y$)\} )
\\[0ex]6. ${\it xm}$(\{$y$:$T$$\mid$ $P$($y$)\} ) = $z$
\\[0ex]$\vdash$  case $z$ of inl($z$) =$>$ $z$ $\mid$ inr($w$) =$>$ "???" $\in$ $T$